(set-option :produce-proofs true)

(declare-const x Bool)
(declare-const y Bool)
(declare-const z Bool)

; we define our conjecture
(define-fun conjecture () Bool
	(=> (and (xor x y) (= y z))
	    (and x z)))

; subsequently we assert the negation to check for validity
(assert (not conjecture))

; check validity of conjecture by checking whether not conjecture is sat, which would mean there exists a counterexample
(check-sat)
;(get-model)

; we assert a different value for x as a blocking clause to find additional solutions
(assert (not (and (not x) y z)))

(check-sat)
;(get-model)

; we assert a different value for y as a blocking clause to find additional solutions
(assert (not (and x (not y) (not z))))

(check-sat)
; as this formula has become unsat, we retrieve a proof
;(get-proof)